Theorem Proving --------------- [(Up)](../../README.md#topics) | _See also: [Formal Specification](../Formal%20Specification/README.md#formal-specification), [Coq](../Coq/README.md#coq)_ - - - - Works regarding the formal proving of theorems, and the mechanical implementation of such, especially (but not exclusively) as computer software. ### Web resources ### General [The Incredible Proof Machine](https://incredible.pm/) ★★★ [LCF architecture \| PLS Lab](https://www.pls-lab.org/LCF_architecture) ★ [The de Bruijn criterion vs the LCF architecture](https://lawrencecpaulson.github.io/2022/01/05/LCF.html) ★ [John Harrison: Slides from recent talks](https://www.cl.cam.ac.uk/~jrh13/slides/) ★ [Satisfiability modulo theories - Wikipedia](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) [Do theorems provers demonstrate their own correctness?](https://cs.stackexchange.com/questions/119817/do-theorems-provers-demonstrate-their-own-correctness) ★★★ [What is a deep embedding vs a shallow embedding? With examples?](https://proofassistants.stackexchange.com/questions/2499/what-is-a-deep-embedding-vs-a-shallow-embedding-with-examples.) ★ ### HOL (and HOL Light) [HOL Interactive Theorem Prover](https://hol-theorem-prover.org/) ★ [HOL Light](https://www.cl.cam.ac.uk/~jrh13/hol-light/) ★ [HOL Light - Wikipedia](https://en.wikipedia.org/wiki/HOL_Light) [HOL88/src/ml/hol-rule.ml at master · theoremprover-museum/HOL88](https://github.com/theoremprover-museum/HOL88/blob/master/src/ml/hol-rule.ml) ★ ### Lean [notes-fplean/notes at cron - notes-fplean - Codeberg.org](https://codeberg.org/dsby/notes-fplean/src/branch/cron/notes) ★ ### F* [F\*: A Higher-Order Effectful Language Designed for Program Verification](https://www.fstar-lang.org/) ★ [F\* Tutorial](http://www.fstar-lang.org/tutorial/) ★ [Calculational proofs · FStarLang/FStar Wiki](https://github.com/FStarLang/FStar/wiki/Calculational-proofs) ★ [Executing F\* code · FStarLang/FStar Wiki](https://github.com/FStarLang/FStar/wiki/Executing-F%2A-code) ★ [Proof-oriented Programming in F\*](https://fstar-lang.org/gs2021/gs2021.html#/sec-proof-oriented-programming-in-f-) ★ [💭](commentary/cpressey.md#proof-oriented-programming-in-f) [F\* - An introduction to the F\* programming language](https://web.archive.org/web/20190609084718/https://rise4fun.com/FStar/tutorialcontent/guide) ★ [Program verification with F\*](https://prosecco.gforge.inria.fr/personal/hritcu/teaching/vtsa2019/) ★ [💭](commentary/cpressey.md#program-verification-with-f) ### Other [Metamath Home Page](https://us.metamath.org/index.html) ★ [Ulrich Berger, Minlog (wayback)](https://web.archive.org/web/20210506214300/http://www.cs.swan.ac.uk/~csulrich/minlog.html) ★ _(in [Equational Logic](../Equational%20Logic/README.md#equational-logic))_ [Formal verification of simple equational proofs (as in Universal Algebra\...)?](https://mathoverflow.net/questions/71265/formal-verification-of-simple-equational-proofs-as-in-universal-algebra) ★ ### Repositories [stepchowfun/proofs: My personal repository of formally verified mathematics.](https://github.com/stepchowfun/proofs) ★★ _(in [Name Binding](../Name%20Binding/README.md#name-binding))_ [bacam/sato-maps-agda](https://github.com/bacam/sato-maps-agda) ★ [💭](commentary/cpressey.md#bacam-sato-maps-agda) ### Papers Robbins Algebras are Boolean (online @ [www.cs.unm.edu](https://www.cs.unm.edu/~mccune/papers/robbins/)) ★ [💭](commentary/cpressey.md#robbins-algebras-are-boolean) How to believe a machine-checked proof (online @ [tidsskrift.dk](https://tidsskrift.dk/brics/article/view/18945)) ★ [💭](commentary/cpressey.md#how-to-believe-a-machine-checked-proof) Automated Reasoning and its Applications (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/slides/hanoi-30jul09/slides.pdf)) [💭](commentary/cpressey.md#automated-reasoning-and-its-applications) The LCF Approach to Theorem Proving (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/slides/manchester-12sep01/slides.pdf)) ★ [💭](commentary/cpressey.md#the-lcf-approach-to-theorem-proving) From LCF to HOL (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/archive/mjcg/papers/HolHistory.pdf)) Automated Reasoning for the Working Mathematician (online @ [www.contrib.andrew.cmu.edu](https://www.contrib.andrew.cmu.edu/~avigad/Talks/london)) ★ [💭](commentary/cpressey.md#automated-reasoning-for-the-working-mathematician) The Future of Mathematics? (online @ [www.andrew.cmu.edu](https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf)) ★★★ [💭](commentary/cpressey.md#the-future-of-mathematics) HOL Light - tutorial.pdf (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf)) ★ Theorem proving support in programming language semantics (online @ [arxiv.org](https://arxiv.org/abs/0707.0926)) ★ [💭](commentary/cpressey.md#theorem-proving-support-in-programming-language-semantics) Towards self-verification of HOL Light (online @ [www.cl.cam.ac.uk](https://www.cl.cam.ac.uk/~jrh13/papers/holhol.pdf)) A Self-Verifying Theorem Prover (online @ [www.kookamara.com](https://www.kookamara.com/jared/dissertation.pdf)) Hyperproof: Logical Reasoning with Diagrams (online @ [aaai.org](https://aaai.org/papers/0016-ss92-02-016-hyperproof-logical-reasoning-with-diagrams/)) ★★ ### Books The Seventeen Provers of the World (borrow with print disabilities @ [archive.org](https://archive.org/details/seventeenprovers00free)) ★ [💭](commentary/cpressey.md#the-seventeen-provers-of-the-world) Theorem Proving in Lean 4 (online @ [archive.org](https://leanprover.github.io/theorem_proving_in_lean4/)) ★ [💭](commentary/cpressey.md#theorem-proving-in-lean-4) Handbook of Automated Reasoning, Vol. 1 (borrow with print disabilities @ [archive.org](https://archive.org/details/handbookofautoma0000unse_m2v0)) ★★ Handbook of Automated Reasoning, Vol. 2 (borrow with print disabilities @ [archive.org](https://archive.org/details/handbookofautoma0002unse_r4b9)) ★★ Hyperproof (borrow @ [archive.org](https://archive.org/details/hyperproof0000barw)) ★ [💭](commentary/cpressey.md#hyperproof) Logic Machines and Diagrams (online @ [archive.org](https://archive.org/details/logicmachinesdia00mart)) (borrow @ [archive.org](https://archive.org/details/logicmachinesdia0000unse)) ★★ [💭](commentary/cpressey.md#logic-machines-and-diagrams)